Nuprl Lemma : discrete_struct_wf
0,22
postcript
pdf
A
:Type{i}. discrete_struct{i:l}(
A
)
Type{i'}
latex
Definitions
DS(
A
)
,
EqDecider(
T
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
deq
wf
origin
A:Type{i}. discrete_struct{i:l}(A) 
Type{i'} A:Type{i}. discrete_struct{i:l}(A) Type{i'} x:A. B(x) T